Inference at * 1 
Iof proof for Lemma order functionality wrt iff:



1. T : Type
2. R : TT
3. R' : TT
4. x, y:T. R(x,y)  R'(x,y)
  (Refl(T;x,y.R(x,y)) & Trans(T;x,y.R(x,y)) & AntiSym(T;x,y.R(x,y)))
   (Refl(T;x,y.R'(x,y)) & Trans(T;x,y.R'(x,y)) & AntiSym(T;x,y.R'(x,y))) 

latex

 by InteriorProof ((RWH (HypC 4) 0) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n
CollapseTHENA ((Au),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1:   (Refl(T;x,y.R'(x,y)) & Trans(T;x,y.R'(x,y)) & AntiSym(T;x,y.R'(x,y)))
C1:    (Refl(T;x,y.R'(x,y)) & Trans(T;x,y.R'(x,y)) & AntiSym(T;x,y.R'(x,y)))
C.

Definitions	P  Q, P  Q, P  Q, x:A. B(x), x,y. t(x;y), P & Q, t  T, x(s1,s2),
Lemmas	anti sym functionality wrt iff, trans functionality wrt iff, refl functionality wrt iff, and functionality wrt iff, iff functionality wrt iff, anti sym wf, trans wf, refl wf